<html>
<body>
Reports any calls to
<b>java.util.Random.getDouble()</b> which are then multiplied
by some factor and cast to an integer. For generating a random integer in some range,
<b>java.util.Random.getInt()</b> is more efficient.
<!-- tooltip end -->
<p>

</body>
</html>